|
| 1: |
|
circ(cons(a,s),t) |
→ cons(msubst(a,t),circ(s,t)) |
| 2: |
|
circ(cons(lift,s),cons(a,t)) |
→ cons(a,circ(s,t)) |
| 3: |
|
circ(cons(lift,s),cons(lift,t)) |
→ cons(lift,circ(s,t)) |
| 4: |
|
circ(circ(s,t),u) |
→ circ(s,circ(t,u)) |
| 5: |
|
circ(s,id) |
→ s |
| 6: |
|
circ(id,s) |
→ s |
| 7: |
|
circ(cons(lift,s),circ(cons(lift,t),u)) |
→ circ(cons(lift,circ(s,t)),u) |
| 8: |
|
subst(a,id) |
→ a |
| 9: |
|
msubst(a,id) |
→ a |
| 10: |
|
msubst(msubst(a,s),t) |
→ msubst(a,circ(s,t)) |
|
There are 10 dependency pairs:
|
| 11: |
|
CIRC(cons(a,s),t) |
→ MSUBST(a,t) |
| 12: |
|
CIRC(cons(a,s),t) |
→ CIRC(s,t) |
| 13: |
|
CIRC(cons(lift,s),cons(a,t)) |
→ CIRC(s,t) |
| 14: |
|
CIRC(cons(lift,s),cons(lift,t)) |
→ CIRC(s,t) |
| 15: |
|
CIRC(circ(s,t),u) |
→ CIRC(s,circ(t,u)) |
| 16: |
|
CIRC(circ(s,t),u) |
→ CIRC(t,u) |
| 17: |
|
CIRC(cons(lift,s),circ(cons(lift,t),u)) |
→ CIRC(cons(lift,circ(s,t)),u) |
| 18: |
|
CIRC(cons(lift,s),circ(cons(lift,t),u)) |
→ CIRC(s,t) |
| 19: |
|
MSUBST(msubst(a,s),t) |
→ MSUBST(a,circ(s,t)) |
| 20: |
|
MSUBST(msubst(a,s),t) |
→ CIRC(s,t) |
|
The approximated dependency graph contains one SCC:
{11-20}.